Model completeness
A theory T'' is '''model complete' if it satisfies one of the following equivalent conditions: # Whenever M'' ⊆ '' N is an inclusion of models of T'', ''M is an elementary substructure of N''. # Every model of ''T is existentially closed. # Every formula \phi(x) is equivalent, mod T'', to a universal formula. # Every formula is equivalent, mod ''T, to an existential formula. # Every universal formula is equivalent, mod T'', to an existential formula. # Every existential formula is equivalent, mot ''T, to a universal formula. See below for a proof that these notions are equivalent. Examples Theories with quantifier elimination are model complete. This includes ACF, RCF (in the language with ≤), DLO, and ACVF. Even in the pure field language, RCF is model complete, because x'' ≤ ''y admits an existential definition : \exists z : y - x = z^2 and a universal definition : \forall z, w : w(x - y) \ne 1 \vee z^2 \ne (x - y) Another notable model complete theory, without quantifier elimination, is ACFA. Proof that the definitions are equivalent Conditions (3) and (4) are equivalent by De Morgan's Laws: \phi(x) is equivalent to a universal formula if and only if \neg \phi(x) is equivalent to an existential formula. Conditions (5) and (6) are similarly equivalent. Conditions (3-4) clearly imply (5-6). Conversely, assume (5-6). We show by induction on n'' that any formula of the form : \forall y_1 \exists y_2 \forall y_3 \cdots Q y_n : \phi(x,y_1,\ldots,y_n) is equivalent to a universal formula, where the ''yi'''s are tuples, ''Q is the appropriate quantifier, and \phi is quantifier-free. The base case where n'' = 1 is trivial. For ''n > 1, the inductive hypothesis implies that : \neg \exists y_2 \forall y_3 \cdots Q y_n : \phi \equiv \forall y_2 \exists y_3 \cdots \neg \phi , must be equivalent to a universal formula. Consequently, : \exists y_2 \forall y_3 \cdots Q y_n : \phi is equivalent to an existential formula. By condition (6), it is equivalent to some universal formula : \forall z : \psi(x;y_1;z) Then the original formula is equivalent to : \forall y_1 \forall z : \psi(x;y_1;z) which is a universal formula. This completes the inductive proof that any formula in prenex form is equivalent to a universal formula. Any formula can be put in prenex form, so condition (3) holds. So conditions (3-6) are all equivalent. It remains to show that (1) implies (2) implies (3-6) implies (1). Suppose (1) holds, and let us prove (2). We need to prove that whenever M'' ⊆ ''N is an inclusion of models of T'', then ''M is existentially closed in M''. This means that for every existential formula \phi(x) and every tuple ''a from M'', we have : M \models \phi(a) \iff N \models \phi(a) Obviously this is a weaker condition than ''M being an elementary substructure of N'', so (1) certainly implies (2). Now assume (2). Then whenever ''M ⊆ N'' is an inclusion of models of ''T, M'' is existentially closed in ''T. So if \phi(x) is a formula and c'' is a tuple from ''M, then : M \models \phi(a) \implies N \models \phi(a) But this is one of the characterizations of universal formulas, so \phi(x) must be equivalent (mod T'') to a universal formula. Therefore (6) holds. Finally, assume (3-6). Let ''M ⊆ N'' be an inclusion of models. We need to show that ''M is an elementary substructure of N''. Let \phi(x) be a formula, and ''c be a tuple from M''. We need to show that : M \models \phi© \iff N \models \phi© \qquad (*) By (3) and (4), we can find existential and universal formulas \psi(x) and \chi(x) , respectively, which are equivalent mod ''T to \phi(x) . Now universal formulas are always preserved downwards, and existential formulas are preserved upwards, so : N \models \psi© \implies M \models \psi© : M \models \chi© \implies M \models \chi© As \phi(x) , \psi(x) , and \chi(x) are all equivalent, we obtain the desired (*) above. QED.